es:ES, a, e:E.
(isrcv(a))
 (isrcv(e))
 ((first(sender(e))))
 a loc pred(sender(e)) 
 (sender(a) < e) 

latex

Definitions	t  T, P  Q, x:A. B(x), , x  {FDLNOr12445}
Lemmas	event system wf, es-E wf, es-isrcv wf, es-first wf, assert wf, not wf, es-le wf, es-causle weakening, es-causl transitivity2, es-pred wf, es-causle weakening locl, es-sender wf, es-pred-causl, es-sender-causl